COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		To understand our view about what practical computer-aided
C00009 ENDMK
C⊗;
	To understand our view about what practical computer-aided
program verification requires, we need some history.

	(McCarthy 1960) contained the first proposals that debugging
of computer programs be replaced by computer checked proofs that
a program meets its specifications.  (McCarthy 1963a and 1963b), which
are still often referenced, proposed some informal methods for
proving properties of recursive programs.  (McCarthy 1964) and
(McCarthy and Painter 1967) were the first papers to discuss
proving properties of compilers, and the latter paper proved the
correctness of a simple compiler.  (Floyd 1967) was the first paper
to give a proof method for sequential programs.

	Starting in the late 1960s program verification became an
important subfield of computer science with work by Floyd, Manna,
Scott, Dijkstra, Morris, Wegbreit, Vuillemin,  Boyer, Moore
and others.  As with all fields that attract mathematical interest,
purely mathematical considerations have come to dominate the thinking
of some researchers, and their interests have become detached from
any practical goals.  (References will be supplied on request).
While
much progress has been made, neither automatic verification nor
interactive computer-checked verification has come into practical
use.

	More recently the practical importance of verification has
been recognized and applied research programs aimed at this goal
have been started.  In our opinion, this work has reasonable prospects
of contributing practical techniques in the short run to some
verification goals, but other practical goals require different
ideas than those now popular.  Here are some contentions:

	Classical input-output specifications are inadequate
in that they don't allow stating equivalences of programs or
more generally relations between functions computed by programs.

	Formalisms that only treat objects occuring in the
program are inadequate.  The correctness of a program often
depends on reasoning about objects not directly present in
the program.  For example, ...
algebraic relations and inadequacy of input-output specs
importance of other entities than occur in the program
logic programming
importance of logic as specification language
connectins with recursive function and abstract computability
importance of interactive theorem proving
there is still a long way to go
characterization of programs in first order logic
	1. 

******

	Our work on verification is divided into two categories:

1. Inventing formalisms for proofs of program properties.

2. Interactive theorem proving.

	Both of these efforts have a long history.  [McCarthy 1963a], of
which a preliminary version appeared in 1961 was probably the first
paper to give a formal method for proving facts about recursive
programs.  (McCarthy 1960) was probably the first paper to propose
that debugging be replaced by a computer checked proof of program
correctness.  [McCarthy 1963b] was the first paper to give the
formal definition of the correctness of a compiler and
[McCarthy 1967] was probably the first paper to prove
the correctness of a compiler.

	[Abrahams 1962], a thesis written under McCarthy's direction,
was the first paper to describe a computer program for checking mathematical
proofs.

	Our present theoretical efforts are based on the following:

	1. [Cartwright and McCarthy 1979] gives a way of representing
recursive programs by sentences and schemata of first order logic
that is complete relative to the data domain and its axiomatization.
Namely, and sentence about the program, can be proved equivalent to
a first order sentence involving only the functions and predicates of the data
domain.  Thus no further axioms or rules of inference are required
to prove properties of the function defined by the program.

	2. The technique has proved practical and is now taught
to beginning LISP students.  This Fall, for the first time, they
will prove their pure LISP programs correct using the EKL interactive
theorem prover.

	3. Carolyn Talcott is developing a general

	4.